/**
 *  TiniSatJ :: A Java implemented SAT Solver based on Tinisat 0.22
 *
 *  Copyright (C) 2007 KITAGAWA, Satoshi.
 *
 *  Original TiniSat is available from
 *  http://users.rsise.anu.edu.au/~jinbo/tinisat/
 *
 *  This program is free software; you can redistribute it and/or modify
 *  it under the terms of the GNU General Public License as published by
 *  the Free Software Foundation; either version 2 of the License, or
 *  (at your option) any later version.
 *
 *  This program is distributed in the hope that it will be useful,
 *  but WITHOUT ANY WARRANTY; without even the implied warranty of
 *  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
 *  GNU General Public License for more details.
 *
 *  You should have received a copy of the GNU General Public License
 *  along with this program; if not, write to the Free Software
 *  Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA
 */

package com.googlecode.tinisat_j;
import java.io.FileInputStream;
import java.io.FileNotFoundException;
import java.io.IOException;
import java.nio.ByteBuffer;
import java.nio.channels.FileChannel;
import java.util.HashSet;


public class Cnf {
	private FileChannel in;
	private ByteBuffer buff;

    public int vc;            // var count
    public int cc;            // clause count
    public int[][] clauses;
    public int lc;            // literal count
    public int[] cl;        // clause length

	private int load() throws IOException {
		buff.clear();
		int size = in.read(buff);
		buff.flip();
		return size;
	}

	private int parseInt(int lit) throws IOException {
		while ( true ) {
			char ch = (char) buff.get();
			if ( Character.isDigit(ch) ) {
				lit *= 10;
				lit += (ch - '0');
			}
			else {
				break;
			}
		}
		return lit;
	}

	private void parseProblem() throws IOException {
		int[] num = new int[2];
		int idx = 0;
		char ch = '\n';
		while ( idx < 2 ) {
			ch = (char) buff.get();
			if (ch == '\n') break;
			if (Character.isDigit(ch)) {
				num[idx++] = parseInt(ch - '0');
			}
		}

		vc = num[0];
		cc = num[1];
        clauses = new int[cc][];
        cl = new int[cc];
	}

	private void skipLine() throws IOException {
		while ( true ) {
			char ch = (char) buff.get();
			if (ch == '\n') break;
		}
	}

	public void parse(String fname) {
		try {
			in = new FileInputStream(fname).getChannel();
			buff = ByteBuffer.allocateDirect((int)in.size());
			load();

            int nCla = 0;
            int nLit = 0;

            HashSet<Integer> lSet = new HashSet<Integer>();
            boolean skip = false;

			while ( buff.hasRemaining() ) {
				char ch = (char) buff.get();

				if (!skip && (ch == '-' || ('1' <= ch && ch <= '9'))) {
					int lit = 0;
					if (ch == '-') lit = -parseInt(0);
					else lit = parseInt(ch-'0');

					if (lSet.contains(-lit)) {
                        skip = true;
                    }
                    else if (!lSet.contains(lit)){
                        lSet.add(lit);
                        nLit++;
                    }
				}
				else if (ch == '0') {
					// create new clause
                    if (!skip) {
                        int [] lits = new int[nLit+1];
                        int j = 0;
                        for (int i : lSet) {
                            lits[j++] = i;
                        }
                        lits[nLit] = 0;
                        clauses[nCla++] = lits;
                    }
                    skip = false;
                    lc += nLit;
                    nLit = 0;
                    lSet.clear();
				}
				else if (ch == 'c') skipLine();
				else if (ch == 'p') parseProblem();
			}
            if (nCla < cc) {
                //clauses = Arrays.copyOf(clauses, nCla);
                int[][] clauses_ = new int[nCla][];
                System.arraycopy(clauses, 0, clauses_, 0, nCla);
            }
			in.close();
		} catch (FileNotFoundException e) {
			// TODO Auto-generated catch block
			e.printStackTrace();
		} catch (IOException e) {
			// TODO Auto-generated catch block
			e.printStackTrace();
		}
	}

    public void show() {
        for (int i=0; i<clauses.length; i++) {
            System.out.print("Clause " + i + " :: ");
            for (int j=0; j<clauses[i].length; j++) {
                System.out.print(clauses[i][j] + " ");
            }
            System.out.print("\n");
        }
    }
	/**
	 * @param args
	 */
	public static void main(String[] args) {
		// TODO Auto-generated method stub
		Cnf t = new Cnf();
		long tic = System.currentTimeMillis();
		t.parse(args[0]);
		long toc = System.currentTimeMillis();
		System.out.println("\n" + (toc-tic));

		t.show();
	}

}
